%Section~\ref{s:major-proposals} quickly tours through the major recent proposals for adding immutability while extracting the common themes and highlighting the differences.

\section{A Selection of Recent Immutability Proposals}
\label{s:major-proposals}

We will now present in more detail the major proposals improving
on the status quo in modern popular OO languages, i.e., \kw{final} in
Java and \Cconst{} in C++. Javari~\cite{TschantzE2005} was
presented in 2004, adding read-only references. In 2007
Immutability Generic Java (IGJ)~\cite{zibin:2007:immutability} was
proposed, adding immutability and immutability parameterization.
\Joe~\cite{oestlund:2008:oui}, proposed in 2008, uses ownership,
external uniqueness --- to support transition from mutable to
immutable --- and a trivial effects system to support immutability
and context-based immutability. OIGJ~\cite{zibin:2010:oigj},
published in 2010, again employs ownership to achieve
immutability, albeit a less strict variant of ownership allowing
for more flexibility. OIGJ uses the existing Java generics
machinery to encode ownership, which removes the need for an extra
parameter clause on classes and methods. While we describe the proposals by the authors of this chapter in great detail, we also provide an overview of the other complementary proposals in the Section~\ref{ss:others}.


\subsection{Javari}

The Javari~\cite{TschantzE2005} programming language extends Java to allow programmers to
specify and enforce reference immutability constraints.
A read-only reference cannot be used to modify the object, including its
transitive state, to which it refers.

Javari's type system differs from previous proposals (for Java, C++,
and other languages) in a number of ways.
First, it offers reference, not object,
immutability. Second, Javari offers guarantees for the entire transitively reachable
state of an object --- the state of the object and all state reachable
by following references through its (non-static) fields.
A programmer may use the type system to support reasoning about either
the representation state of an object or its abstract state;
to support the latter, parts of a class can be marked as not part of
its abstract state.

Third, Javari combines static and dynamic checking in
a safe and expressive way.  Dynamic checking is necessary only for programs
that use immutability downcasts, but such downcasts can be convenient for
interoperation with legacy code or to express facts that cannot be proved
by the type system.  Javari also offers parameterization over
immutability.

Experience with over 160,000 lines of Javari code, including the Javari
compiler itself, indicates that Javari is effective in practice in helping
programmers to document their code, reason about it, and prevent and
eliminate errors.

The language design issues include the following:
\begin{itemize} \itemsep 0pt \parskip 0pt
\item
  Should Javari use new keywords (and possibly other syntax) to indicate
  reference immutability, or should it use Java's annotation
  mechanism\footnote{\url{http://java.sun.com/j2se/1.5.0/docs/guide/language/annotations.html}}?
  (Or, should a prototype implementation use annotations, even if Javari
  itself should eventually use keywords?)
\item
  The immutability downcast adds expressiveness to the Javari language, but
  it also adds implementation complexity and (potentially pervasive)
  run-time overhead.  Is a language that lacks immutability downcasts
  practical?
\item
  How can uses of reflection, serialization, and other Java constructs that
  are outside the scope of the Java type system be handled, particularly
  without adding run-time overhead?
\item
  The existing Javari template mechanism is unsatisfactory.  It is
  orthogonal to Java generics (even in places where it seems that generics
  should be a satisfactory solution).
%  Can we use Java generics in place of
%  templates?  Or, can we use generics where possible and reduce the scope
%  and power of templates in other situations?  Or, should we use
%  polymorphic types of some sort?
%  See the ``Parameterized Types'' document.
\end{itemize}

%Implementation design issues include the following:
%\begin{itemize} \itemsep 0pt \parskip 0pt
%\item
%  Eventually, we must provide type checking both in the context of the
%  Javari compiler, and in the context of the JVM (as part of byte code
%  verification).  Should we write just a byte code type-checker and invoke
%  it from the compiler, or should we write two different type checkers?  If
%  we select the latter, it is probably enough to start with the source code
%  type checker, leaving the byte code verifier until much later in the
%  project.
%  What tools should the type checking implementation build upon? (For
%  example, should a source code type checker be built into \mytt{javac} or as a
%  stand-alone tool?)
%\item
%  Should we convert the two .class files into one at load time, after
%  verification?
%  Javari must interoperate with code compiled by existing Java compilers.
%  (It does so by compiling a \mytt{.javari} into two \mytt{.class} files,
%  one of which has a ``mangled'' name.)  Java (and Javari) compilers will
%  never produce ...
%  \item
%    In the long run, a type inference tool will be required.
%    Must we build this tool early in the project, or can we
%    delay it?
%    Should such a tool operate on source code or on
%    \mytt{.class} files?
%\end{itemize}

Javari has presented a type system that is capable of expression,
compile-time verification, and run-time checking of reference
immutability constraints.  Read-only references guarantee that the
reference cannot be used to perform any modification of a
(transitively) referred-to object.  The type system should be
generally applicable to object-oriented languages, but for
concreteness we have presented it in the context of Javari, an
extension to the full Java 5 language, including generic types,
arrays, reflection, serialization, inner classes, exceptions, and
other idiosyncrasies.  Immutability polymorphism (templates) for
methods are smoothly integrated into the language, reducing code
duplication.  Tschantz~et~al.~\cite{TschantzE2005} provided a set of formal type rules for a core
calculus that models the Javari language and used it to prove
type soundness for the Javari type system.

Javari provides a practical and effective combination of language
features.  For instance, we describe a type system for reference
rather than object immutability.  Reference immutability is useful in
more circumstances, such as specifying interfaces, or objects that are
only sometimes immutable.  Furthermore, type-based analyses can run
after type checking in order to make stronger guarantees (such as
object immutability) or to enable verification or transformation.  The
system is statically type-safe, but optionally permits downcasts that
transform compile-time checks into run-time checks for specific
references, in the event that a programmer finds the type system too
constraining.  The language is backward compatible with Java and the
Java Virtual Machine, and is interoperable with Java.  Together with
substantial experience with a prototype for a closely related
dialect~\cite{BirkaE2004}, these design features provide evidence that
the language design is effective and useful.

The Javari language presented is an evolutionary improvement
of an earlier dialect~\cite{BirkaE2004}, which we call ``Javari2004''. In what follows we highlight the main features of the Javari language and justify them in the context of a large user study done using the previous version of the language.


\subsubsection{Distinguishing assignability from mutability}

Javari2004's \mutable{} keyword declares that a field is both assignable
and mutable:  there is no way to declare
that a field is only assignable or only mutable.
Javari's \assignable{} and \mutable{} keywords
highlight the orthogonality of assignability and
mutability, and increase the expressiveness of the language.
See appendix of Javari paper for examples of the use
of \assignable{} and \mutable{}.


\subsubsection{Generic types}

Javari provides a detailed treatment of generic
classes that smoothly integrates read-only references with them.
Javari2004 does not supports generic classes, though the OOPSLA 2004 paper
speculates about a macro expansion mechanism that is
syntactically, but not semantically, similar to the way that Java 5 treats
type parameters.  Java 5 compiles type parameters via type erasure, but
Javari2004 treated the mutability parameters (which appeared in the same
list as the type parameters) via code duplication; this distinction
complicates implementation, understanding, and use.

%Javari2004 also proposed that a generic class could declare whether a field
%whose type is a type parameter is a part of the object's abstract state.
%We have discovered that such a declaration makes no sense.  For a field
%whose type is a type parameter to be a part of the object's abstract state,
%it must be this-mutable; however, such a field cannot be this-mutable
%.  Javari also disallows type
%parameters be modified with the \mutable{} keyword.


\subsubsection{Arrays}

As with generic classes, Javari permits programmers to independently
specify the mutability of each level of an array.
By contrast,
Javari2004's specification states: ``\jv{readonly int[][]} and \jv{readonly
  (readonly int[])[]} are equivalent,'' forbidding creation of
a read-only array of mutable items.

Within current Javari one may make such as declaration as follows:
\jv{readonly Object[]}.  One could also declare a mutable array of
read-only objects: \jv{/*mutable*/ (readonly Object)[]}.


\subsubsection{Method templates}

Javari2004 integrated the syntax for templating a
method over mutability with the syntax for Java 5's generic types.

For example, the following method signature is a templated method.

\begin{java}
public <RO> RO List<RO Invariant> get(RO PptTopLevel ppt) RO;
\end{java}
% \begin{verbatimfont}
% \begin{Verbatim}[commandchars=\|\[\],commentchar=\!]
% public <RO> RO List<RO Invariant> get(RO PptTopLevel ppt) RO;
% \end{Verbatim}
% \end{verbatimfont}
The \jv{<RO>} at the beginning of the signature specifies that \jv{RO}
is a type parameter.

Whether a parameter is intended to be a normal type parameter or a
mutability type parameter must be inferred from its usage, greatly
complicating a compiler (and the
prototype Javari2004 implementation required distinct syntax to ease the
compiler's task~\cite{Birka2003:TR,BirkaE2004}).

Furthermore, Javari2004 allows declaring an arbitrary number of
mutability type parameters.
Only a single mutability type parameter was deemed
sufficient by the Javari designers, so 
Javari uses a much simpler mechanism (\romaybe{}) for indicating a variable
mutability.
This new approach highlights the orthogonality of the Java 5's
generic types and Javari's mutability polymorphism for methods.
Furthermore, it does not require any run-time representation of the
polymorphism. IGJ~\cite{zibin:2007:immutability} and OIGJ~\cite{zibin:2010:oigj} have both demonstrated that building on generic types provides a much nicer treatment for immutability parameterization completely removing the need for \romaybe{}.

% Alex: The below are too short/vague to be useful for this chapter:

%\subsubsection{Reflection and serialization}
%
%Reflection and serialization create objects whose
%types are not known to the static type checker.
%In Javari2004 (as in many other proposed type systems for Java), reflection
%and serialization create loopholes in the type system.
%The current Javari language is sound with respect to reflection and
%serialization, by introducing quick, local checks that can be performed at
%run time. 
%
%
%\subsubsection{Dynamic cast checking}
%
%The Javari2004 paper proposes an implementation of dynamic checking that
%requires associating a ``readonly'' Boolean ``read only bit x'' with each reference
%\mytt{x} (\emph{not} with each object).  Such an implementation can be
%performed relatively efficiently in a JVM, but changing a JVM is a
%difficult task and is infeasible for incremental adoption.  Furthermore,
%the implementation is slightly awkward to implement efficiently via
%classfile rewriting. 

% We have proposed a simpler implementation that works via interfaces and wrapper objects.


\subsection{IGJ}

\emph{Immutability Generic Java} (IGJ) is a language
that supports class and object immutability and read-only references.
Each object is either mutable or immutable, and each reference is
\Immutable, \Mutable, or \ReadOnly.  Inspired by work that combines
ownership and generics~\cite{PotaninNCB2006}, the distinctions are
expressed without changing Java's syntax by adding one new type
parameter (at the beginning of the list of type parameters):
%
\begin{java}
  // ^(An immutable reference to an immutable date; mutating the)^
  // ^(referent is prohibited, via this or any other reference.)^
  Date<Immutable> immutD = new Date<Immutable>();
  // ^(A mutable reference to a mutable date; mutating the referent)^
  // ^(is permitted, via this or any other mutable reference.)^
  Date<Mutable> mutD = new Date<Mutable>();
  // ^(A read-only reference to any date; mutating the referent is)^
  // ^(prohibited via this reference, but the referent may be changed)^
  // ^(via an aliasing mutable reference.)^
  Date<ReadOnly> roD = ^($\cdots$)^ ? immutD : mutD;
\end{java}
%
Line 3 shows object immutability in IGJ, and Line 10 shows
read-only references.

Java prohibits changes to type arguments, such as in Line 10, to
avoid a type loophole. More detailed discussion of the Java
language and type system is given by Bracha
et~al.~\cite{BrachaOSW98} and Igarashi
et~al.~\cite{Igarashi:2001:FJM}.  Line 10 is legal in IGJ, because
IGJ allows covariant changes in the immutability parameter.  IGJ
even allows covariant changes in other type parameters if mutation
is disallowed, e.g.,
\code{List}\discretionary{}{}{}\code{\hgn{{\ReadOnly},Integer}} is
a subtype of \code{List\hgn{{\ReadOnly},Number}}.

IGJ satisfies the following design principles:
\begin{description}
  \item[Transitivity]

    More accurately, IGJ does not require transitivity.  Rather, it
    provides a mechanism by which programmers can specify exactly
    where transitivity should be applied --- and then that transitivity
    is enforced by the type system.

    IGJ provides transitive (deep) immutability that protects the
    entire abstract state of an object.  For example, an immutable
    graph contains an immutable set of immutable edges.
    
    \CC{} does not support such transitivity because its
    \const-guarantee does not traverse pointers, i.e., a pointer in a
    \const{} object can mutate its referent.

    IGJ also permits excluding a field from the abstract state.
    For example, fields used for caching can be mutated even in an
    immutable object.

  \item[Static] 

    IGJ has no runtime representation for immutability, such as an
    ``immutability bit'' that is checked before assignments or method
    calls.  IGJ designers believe that testing at runtime whether an object is
    immutable~\cite{SkoglundW2001} hampers program understanding.

    The IGJ compiler works by type-erasure, without any run-time
    representation of reference or object immutability, which enables
    executing the resulting code on any JVM without runtime penalty.
    A similar approach was taken by Generic Java
    (GJ)~\cite{BrachaOSW98} that extended Java 1.4.  As with GJ,
    libraries must either be retrofitted with IGJ types, or fully
    converted to IGJ, before clients can be compiled.  IGJ is backward
    compatible: every legal Java program is a legal IGJ program.
    
%    The principle of erasure is not true due to the relaxed subtyping
%    rules... \COMMENTJOHAN{This sentence needs closing.}

  \item[Polymorphism]
    
    IGJ abstracts over immutability without code duplication by using
    generics and a flexible subtype relation.  For instance, all the
    collection classes in \mbox{\CC's} STL have two overloaded
    versions of \code{iterator}, \code{operator[]}, etc.  The
    underlying problem is the inability to return a reference whose
    immutability depends on the immutability of \this:

    \begin{java}
      const Foo& getFieldFoo() const;
             Foo& getFieldFoo();
    \end{java}

  \item[Simplicity]

    IGJ does not change Java's syntax.  A small number of additional
    typing rules make IGJ more restrictive than Java.  On the other
    hand, IGJ's subtyping rules are more relaxed, allowing covariant
    changes in a type-safe manner.
    
    Phrased differently, IGJ uses rules which fit naturally into
    Java's design.
\end{description}

Most of the IGJ terminology was borrowed from
Javari~\cite{TschantzE2005} such as assignable, readonly, mutable, and
\this-mutable.  In Javari, \this-mutable fields are mutable as lvalue
and readonly as rvalue.  Javari does not support object immutability,
and its read-only references are more limited than that of IGJ because
Javari has no \this-mutable parameters, return types, or local
variables. Javari's keyword \romaybe{} is in essence a template over
immutability.  IGJ uses generics directly to achieve the same goal.

Javari
also supports \this-assignable fields, which pass the assignability
(\keyword{final} or \keyword{assignable}) of \this~to a field.

Finally, Javari uses \code{?\,readonly} which is similar to Java's wildcards.
Consider, for instance, the class \code{Foo} written in Javari's syntax:
%
\begin{java}
class Foo { mutable List<Object> list; }
\end{java}
%
Then in a \code{readonly Foo} the type of \code{list} is
%
\begin{java}
mutable List<? readonly> Object
\end{java}
%
which is syntactic sugar for
%
\begin{java}
mutable List<? extends readonly Object
                 super mutable Object>
\end{java}
%
Thus, it is possible to insert only mutable elements to~\code{list},
and retrieve only read-only elements.  Such complexities, in IGJ designers point of view, make IGJ easier to use than Javari.


\subsection{\Joe}


This section will present \Joe in a bit more detail. \Joe is a
Java-like language with deep ownership, owner-polymorphic methods,
external uniqueness, an effects (revocation) system and a simple
mode system which decorates owners with permissions to indicate
how references with the annotated owners may be used. The
annotation of owners with modes is the main novelty in \Joe. The
modes indicate that a reference may be read or written (\Write{}),
only read (\Read{}), or that the reference is immutable
(\JoeImmutable{}). Read and immutable annotations on an owner in
the class header represent a promise that the code in the class
body will not change objects owned by that owner. The key to
preserving and respecting immutability and read-only in \Joe is a
simple effects system, rooted in ownership types, and inspired by
Clarke and Drossopoulou's
\Joe[1]~\cite{clarke:2002:disjoint}. Classes, and hence objects,
have rights to read or modify objects belonging to certain owners;
only a minor extension to the type system of Clarke and Wrigstad's
\Joline~\cite{CW03b,wrigstad-thesis} is required to ensure that
these rights are not violated.

Classes are parameterized with owners related to each other by an
inside/outside nesting relation. An owner is a permission to
reference the representation of another object. Class headers have
this form:
%
\begin{java}
class List<data- outside owner> { ^($\cdots$)^ }
\end{java}
%
Each class has at least two owner parameters, \this{} and
\owner{}, which represent the representation of the current object
and the representation of the owner of the current object,
respectively. In the example above, the \code{List} class has an
additional permission to reference objects owned by \code{data},
which is nested outside \owner{}. Types are formed by instantiating
the owner parameters, \code{this:List<owner>}. An object with this
type belongs to the representation of the current object and has
the right to reference objects owned by \owner{}. There are two
nesting relations between owners, inside and outside. They exist
in two forms each, one reflexive (\kw{inside}/\kw{outside}) and
one non-reflexive
(\kw{strictly-inside}/\kw{strictly-outside}). Thus, going back to
our list example, a type \code{this:List<this>} denotes a list
object belonging to the current representation, holding objects in
the current representation.

Apart from ownership types, the key ingredients in \Joe are the
following:
\begin{itemize}
\item (externally) unique types (written \code{unique[p]:Object}),
  a special \emph{borrowing} construct for temporarily treating a
  unique type non-uniquely, and \emph{owner casts} for converting
  unique references permanently into normal references.
\item modes on owners --- mutable `\Write{}', read-only `\Read{}',
  and immutable `\JoeImmutable{}'. These appear on every owner
  parameter of a class and owner polymorphic methods, though not
  on types.
\item an effects revocation clause on methods which states which
  owners will not be modified in a method. An object's default set
  of rights is derived from the modes on the owner parameters in
  the class declaration.
\end{itemize}

Annotating owners at the level of classes (that is, for all
instances) rather than types (for each reference) is a
trade-off. Rather than permitting distinctions to be made using
modes on a per reference basis, \Joe admits only per class
granularity. Some potential expressiveness is lost, though the
syntax of types does not need to be extended. Nonetheless, the
effects revocation clauses regain some expressiveness that per
reference modes would give. Another virtue of using per class
rather than per reference modes is that some covariance problems
found in other proposals are avoided, as what you can do with a
reference depends on the context and is not a property of the
reference. The covariance problem, similar to Java generics, is
essentially that immutability variance in the element parameter of
a list makes it possible to mutate read-only elements.



\paragraph{Context-Based Read-Only}

\begin{figure}
\begin{small}
\begin{java}
class ListWriter<o+ outside owner, data- strictlyoutside o> {
  void mutateList(o:List<data> list) {
    list.addFirst(new data:Object());
  }
}
class ListReader<o- outside owner, data+ strictlyoutside o> {
  void mutateElements(o:List<data> list) {
    list.elementAt(0).mutate();
  }
}
class Example {
  void example() {
    this:List<world> list = new this:List<world>();
    this:ListWriter<this, world> w = new this:Writer<this, world>();
    this:ListReader<this, world> r = new this:Reader<this, world>();
    w.mutateList(list);
    r.mutateElements(list);
  }
}
\end{java}
\end{small}
\caption{Different views of the same
  list can exist at the same time. \texttt{r} can modify the elements of
  \texttt{list} but not the \texttt{list} itself, \texttt{w} can
  modify the \texttt{list} object, but not the list's contents, and
  instances of \texttt{Example} can modify both the list and its
  contents.}
\label{fig:reader-writer}
\end{figure}

As shown in Figure \ref{fig:reader-writer}, different clients of
the list can have different views of the same list at the same
time. The class \code{ListReader} does not have permission to mutate
the list, but has no restrictions on mutating the list elements.
Dually, the \code{ListWriter} class can mutate the list but not its
elements.

As owner modes only reflect what a class is allowed to do to
objects with a certain owner, \code{ListWriter} can add data objects
to the list that are read-only to itself and the list, but
writable by \code{Example} and \code{ListReader}. This is a powerful
and flexible idea. For example, \code{Example} can pass the list
to \code{ListWriter} to filter out certain objects in the list.
\code{ListWriter} can then consume or change the list, or copy its
contents to another list, \emph{but not modify them}.
\code{ListWriter} can then return the list to \code{Example}, without
\code{Example} losing its right to modify the objects obtained
from the returned list. This is similar to the context-based
read-only in Universes-based systems \cite{MPH99a,muller-thesis}.
In contrast, however, \Joe does not allow representation exposure via
read-only references.


\paragraph{Immutable Object Initialization}

Immutable objects need to be mutated in their construction
phase. Unless caution is taken the constructor might leak a
reference to \this~(by passing \this~to a method) or mutate other
immutable objects of the same class. The standard solution to this
problem in related proposals is to limit the construction phase to
the constructor
\cite{zibin:2007:immutability,zibin:2010:oigj,haack:2009:obj-imm}. Continuing
initialization by calling auxiliary methods \emph{after} the
constructor returns is simply not possible. \Joe, on the other
hand, permits \emph{staged construction}, as demonstrated in
Figure~\ref{fig:staged-constr}. In this example a client
uses a factory to create an immutable list. The factory creates a
unique list and populates it. The list is then destructively read
and returned to the caller as an immutable.
%
\begin{figure}[t]
\begin{small}
\begin{java}
class Client<p* outside owner, data+ strictlyoutside p> {
  void method() {
    this:Factory<p, data> f = new this:Factory<p, data>();
    p:List<data> immutable = f.createList();
  }
}
class Factory<p* inside world, data+ strictlyoutside p> {
  p:List<data> createList() {
    unique[p]:List<data> list = new p:List<data>();
    borrow list as temp+ l in { // 2nd stage of construct.
      l.add(new data:Object());
    }
    return list--;   // unique reference returned
  }
}
\end{java}
\end{small}
\caption{Staged construction of an immutable list}
\label{fig:staged-constr}
\end{figure}
%
Interestingly enough, if an inference mechanism were employed to
remove trivial uses of borrowing, such as the one in the figure,
then this example could be done without the extra baggage.


\paragraph{Fractional Permissions}

Using uniqueness and \Joline's borrowing statement, \Joe can
encode a variant of Boyland's Fractional
Permissions~\cite{Boy03}, where a mutable reference is turned
into an immutable reference for a limited time, after which it can
be reestablished as a mutable reference with no residual
aliasing. This is described in more detail with an example in
Section \ref{sec:frac_perm}.


\subsection{OIGJ}

This section presents the OIGJ language extension
    that expresses both ownership and immutability information.

OIGJ introduces two new type parameters to each type,
    called the \emph{owner parameter} and the
    \emph{immutability parameter}.
For simplicity of presentation, we assume that the special
    type parameters are at the beginning of the list of type parameters.
We stress that generics in Java are erased during compilation to bytecode
    and do not exist at run time,
    therefore OIGJ does not incur any run-time overhead (nor does it support run-time casts).

In OIGJ, all classes are subtypes of the parameterized root type \code{Object<\underline{O,I}>}
    that declares an owner and an immutability parameter.
In \underline{O}\underline{I}GJ,
    the first parameter is the owner (\underline{O}),
    and the second is the immutability (\underline{I}).
All subclasses must invariantly preserve
    their owner and immutability parameter.
The owner and immutability parameters form two separate hierarchies,
    which are shown in Figure~\ref{Figure:owners-and-immutability-params}.
These parameters cannot be extended, and they have no subtype relation with any other types.
The subtyping relation is denoted by~\st, e.g.,
$\Mutable\st\ReadOnly$.
Subtyping is invariant in the owner parameter and covariant in the immutability parameter.

Note that the \emph{owner parameter} \code{O} is a \emph{type},
    whereas the \emph{owner} of an object is an \emph{object}.
For example, if the owner parameter is \This,
    then the owner is the object \this.
Therefore, the owner parameter (which is a type) at compile time
    corresponds to an owner (which is an object) at run time.
    (See also paragraph \textbf{\emph{Owner vs.\ Owner-parameter}} below.)

OIGJ syntax borrows from
    \emph{conditional Java} (cJ)~\cite{HuangZS2007:cJ},
    where a programmer can write method \emph{guards}.
A guard of the form~\code{\underline{<X extends Y>?} METHOD\_DECLARATION}
    has a dual meaning:
    (i)~the method is applicable only if the type argument that substitutes~\code{X} extends~\code{Y},
    and (ii)~the bound of \code{X} inside \code{METHOD\_DECLARATION} changes to \code{Y}.
The guards are used to express the immutability of \this:  a method
    receiver or a constructor result.  For example,
    a method guarded with \code{\underline{<I extends Mutable>?}} means
    that (i)~the method is applicable only if the receiver is mutable
    and therefore (ii)~\this~can be mutated inside the method.


\begin{figure}[t]
\centering
\includegraphics[scale=0.75]{owners-and-immutability-params}
\caption{The type hierarchy of (a) ownership and (b) immutability parameters.
    \World means the entire world can access the object,
        whereas \This means that \this~owns the object and no one else can access it.
    A \Immut/\Mutable~reference points to an immutable/mutable object.
    A \ReadOnly~reference points to a mutable or immutable object,
        and therefore cannot be used to mutate the object.
    \Raw represents an object under construction whose fields can be assigned.
    }
\label{Figure:owners-and-immutability-params}
\end{figure}


\begin{figure}[h!]
\begin{java}
class Foo<O extends World,I extends ReadOnly> { ^(\label{OIGJEx:decl})^
  // An immutable reference to an immutable date.
  Date<O,Immut> imD = new Date<O,Immut>(); ^(\label{syntax:imD})^
  // A mutable reference to a mutable date.
  Date<O,Mutable> mutD = new Date<O,Mutable>(); ^(\label{syntax:mutD})^
  // A read-only reference to any date.
  // Both ^(\code{roD})^ and ^(\code{imD})^ cannot mutate their referent,
  // however the referent of ^(\code{roD})^ might be mutated by an alias,
  // whereas the referent of ^(\code{imD})^ is immutable.
  Date<O,ReadOnly> roD = ^($\cdots$)^ ? imD : mutD;  ^(\label{syntax:roD})^
  // A date with the same owner and immutability as ^(\this)^.
  Date<O,I> sameD; ^(\label{syntax:sameD})^
  // A date owned by ^(\this)^; it cannot leak.
  Date<This,I> ownedD; ^(\label{syntax:ownedD})^
  // Anyone can access this date.
  Date<World,I> publicD; ^(\label{syntax:publicD})^
  // Can be called on any receiver; cannot mutate ^(\this)^.
  // The method guard ``<^($\cdots$)^>?'' is part of cJ's syntax~^(\cite{HuangZS2007:cJ})^.
  <I extends ReadOnly>? int readonlyMethod() {^($\cdots$)^} ^(\label{OIGJEx:cj:ro})^
  // Can be called only on mutable receivers; can mutate ^(\this)^.
  <I extends Mutable>? void mutatingMethod() {^($\cdots$)^} ^(\label{OIGJEx:cj:mut})^
  // Constructor that can create (im)mutable objects.
  <I extends Raw>? Foo(Date<O,I> d) { ^(\label{OIGJEx:cj:raw})^
    this.sameD = d; ^(\label{OIGJEx:raw:sameD})^
    this.ownedD = new Date<This,I>(); ^(\label{OIGJEx:raw:ownedD})^
    // Illegal, because ^(\code{sameD})^ came from the outside.
    // this.sameD.setTime(^($\cdots$)^); ^(\label{OIGJEx:sameD:setTime})^
    // OK, because ^(\Raw{})^ is transitive for owned fields.
    this.ownedD.setTime(^($\cdots$)^); ^(\label{OIGJEx:ownedD:setTime})^
  } } ^(\label{OIGJEx:cj:raw:end})^
\end{java}
\caption{An example of OIGJ syntax.}
\label{Figure:OIGJ-example}
\end{figure}


\paragraph{Class definition example}
Figure~\ref{Figure:OIGJ-example} shows an example of OIGJ syntax.
A class definition declares
    the owner and immutability parameters (line~\ref{OIGJEx:decl});
    by convention we always denote them by \code{O} and~\code{I}
    and they always extend \World{} and \ReadOnly{}.
If the \code{extends} clause is missing from a class declaration,
    then we assume it extends \code{Object<O,I>}.


\paragraph{Immutability example}
Lines~\ref{syntax:imD}--\ref{syntax:roD} show different kinds of immutability in OIGJ:
    immutable, mutable, and readonly.
A read-only and an immutable reference may seem similar because neither
    can be used to mutate the referent.
However, line~\ref{syntax:roD} shows the difference between the two:
    a read-only reference may point to a mutable object.
Phrased differently, a read-only reference may not mutate its referent,
    though the referent may be changed via an aliasing mutable reference.

Java's type arguments are invariant (neither covariant nor contravariant), to avoid a type
    loophole~\cite{Igarashi:2001:FJM}, so line~\ref{syntax:roD} is
    illegal in Java.
Line~\ref{syntax:roD} is legal in OIGJ, because OIGJ safely allows covariant
    changes in the immutability parameter (but not in the owner parameter).
OIGJ \textit{restricts} Java by having additional typing rules, while at the same time
OIGJ also \textit{relaxes} Java's subtyping relation.
Therefore, neither OIGJ nor Java subsumes the other, i.e.,
    a legal OIGJ program may be illegal in Java (and vice versa).
However, because generics are erased during compilation, the resulting
    bytecode can be executed on any JVM.

The immutability of \code{sameD} (line~\ref{syntax:sameD}) depends on the immutability of \this,
    i.e., \code{sameD} is (im)mutable in an (im)mutable \code{Foo} object.
Similarly, the owner of \code{sameD} is the same as the owner of \this.


\paragraph{Ownership example}
Lines~\ref{syntax:sameD}--\ref{syntax:publicD} show three different owner parameters:
    \hO, \This, and \World.
The owner parameter is invariant, i.e., the subtype relation preserves the owner parameter.
For instance, the types on lines~\ref{syntax:sameD}--\ref{syntax:publicD}
    have no subtype relation with each other because they have different owner parameters.

Reference \code{ownedD} cannot leak outside of \this,
    whereas references \code{sameD} and \code{publicD}
    can potentially be accessed by anyone with access to \this.
Although \code{sameD} and \code{publicD} can be accessed by the same objects,
    they cannot be stored in the same places:
    \code{publicD} can be stored anywhere on the heap (even in a static public variable)
    whereas \code{sameD} can only be stored inside its owner.

We use \Ofn{\ldots} to denote the function that takes a type or a reference, and returns
    its owner parameter;
    e.g.,~$\Ofn{\code{ownedD}}=\This$.
Similarly, function \Ifn{\ldots} returns
    the immutability parameter;
    e.g.,~$\Ifn{\code{ownedD}}=\hI$.
We say that an object~\code{o} is \emph{\this-owned} (i.e., owned by \this)
    if~$\Ofn{\code{o}}=\This$;
    e.g., \code{ownedD} is \this-owned,
    but \code{sameD} is not.
OIGJ prevents leaking \this-owned objects by requiring
    that \this-owned fields (and methods with \this-owned arguments or return-type)
    can only be used via \this.
For example, \code{this.ownedD} is legal, but \code{foo.ownedD} is illegal.


\paragraph{Owner vs.\ owner-parameter}
Now we explain the connection between the \emph{owner parameter}~$\Ofn{o}$,
        which is a generic type parameter at \emph{compile time},
    and the \emph{owner}~$\theta(o)$,
        which is an object at \emph{run time}.
\This is an owner parameter that represents an owner that is the current
  \this~object, and
  \World represents the root of the ownership tree
  (we treat \World both as a type parameter and as an object that is the root of the ownership tree).
Formally, if $\Ofn{o}=\This$ then $\theta(o)=\this$,
    if $\Ofn{o}=\hO$ then $\theta(o)=\theta(\this)$,
    and if $\Ofn{o}=\World$ then $\theta(o)=\World$.
Two references (in the same class) with the same owner parameter (at compile time)
    will point to objects
    with the same owner (at run time),
    i.e., $\Ofn{o_1}=\Ofn{o_2}$ implies $\theta(o_1)=\theta(o_2)$.

Finally, OIGJ provides the following \textit{ownership guarantee}:~$o'$ can point to~$o$ iff~$o' \Oprec \theta(o)$.
By definition of \Oprec, we have that for all~$o$:
    (i)~$o \Oprec o$, (ii)~$o \Oprec \theta(o)$, and (iii)~$o \Oprec \World$.
By part (iii), if~$\theta(o)=\World$ then anyone can point to~$o$.
On lines~\ref{syntax:sameD}--\ref{syntax:publicD}, we see that \this{}
    can point to \code{ownedD}, \code{sameD}, \code{publicD},
    whose owner parameters are~\This, \hO, \World,
    and whose owners are $\this$, $\theta(\this)$, \World.
This conforms with the ownership guarantee according to parts (i), (ii), and~(iii), respectively.
More complicated pointing patterns can occur by using multiple owner parameters,
    e.g., an entry in a list can point to an element owned by the list's owner,
    such as in
    \code{List<\underline{This},I,Date<\underline{O},I>>}.

There is a similar connection between the immutability type parameter (at compile time)
    and the object's immutability (at run time).
Immutability parameter \Mutable~or \Immut~implies the object is mutable or immutable (respectively),
    \ReadOnly~implies the referenced object may be either mutable or
    immutable and thus the object cannot be mutated through the read-only
    reference.
\Raw implies the object is still raw and thus can still be mutated,
        but it might become immutable after it is cooked.


\paragraph{Method guard example}
Lines~\ref{OIGJEx:cj:ro}~and~\ref{OIGJEx:cj:mut} of Figure~\ref{Figure:OIGJ-example} show a read-only and a mutating method.
These methods are \emph{guarded} with \code{<\ldots>?}.
Conditional Java (cJ)~\cite{HuangZS2007:cJ} extends Java with such guards (a.k.a.~conditional type expressions).
Note that cJ changed Java's syntax by using the question mark in
    the guard \code{<\ldots>\underline{?}}.
OIGJ paper uses cJ for convenience.
However, the OIGJ implementation uses type annotations~\cite{JSR308-2008-09-12}
    without changing Java's syntax,
    for conciseness and compatibility with existing tools and code bases.

A guard such as \code{<T extends U>? METHOD\_DECLARATION} has a dual purpose:
    (i)~the method is included only if \code{T extends U},
    and (ii)~the bound of \code{T} is \code{U} inside the method.
In our example, the guard on line~\ref{OIGJEx:cj:mut}
    means that (i)~this method can only be called
        on a \Mutable~receiver, and
        (ii)~inside the method the bound of \code{I} changes to \Mutable.
For instance,
    (i)~only a mutable \code{Foo} object can be a receiver of \code{mutatingMethod}, and
    (ii)~field~\code{sameD} is mutable in \code{mutatingMethod}.
cJ also ensures that the condition of an overriding method is
    equivalent or weaker than the condition of the overridden method.

IGJ used \emph{declaration annotations} to denote
    the immutability of \this.
In this chapter, OIGJ uses cJ to reduce the number of typing rules
    and handle inner classes more flexibly.\footnote{%
      The OIGJ implementation uses \emph{type annotations} to denote
      immutability of \this.  A type annotation \code{@Mutable} on the
      receiver is similar to a cJ \code{<I extends
        Mutable>?} construct, but it separates the distinct roles of the
      receiver and the result in inner class constructors.}
OIGJ does not use the full power of cJ:
    it only uses guards with immutability parameters.
Moreover, we modified cJ to treat guards over constructors
    in a special way.

To summarize, on lines~\ref{OIGJEx:cj:ro}--\ref{OIGJEx:cj:raw}
    we see three guards that change the bound of
    \code{I} to \ReadOnly, \Mutable, and \Raw, respectively.
Because the bound of \code{I} is already declared on line~\ref{OIGJEx:decl} as \ReadOnly{},
    the guard on line~\ref{OIGJEx:cj:ro} can be removed. % without changing the example.


\paragraph{Constructor example}
The constructor on line~\ref{OIGJEx:cj:raw} is guarded with \Raw,
    and therefore can create both mutable and immutable objects, because
    all objects start their life cycle as raw.
This constructor illustrates
    the interplay between \emph{ownership} and \emph{immutability},
    which makes OIGJ more expressive than previous work on immutability.
OIGJ uses ownership information to prolong the \emph{cooking phase} for owned objects:
    the cooking phase
    of \this-owned fields (\code{ownedD}) is longer than that of non-owned fields (\code{sameD}).
This property is critical to type-check the collection classes.

Consider the following code:
%
\begin{java}
class Bar<O extends World,I extends ReadOnly> {
  Date<O,Immut> d = new Date<O,Immut>();
  Foo<O,Immut> foo = new Foo<O,Immut>(d);
}
\end{java}
%
OIGJ provides the following \textit{immutability guarantee}:
    an immutable object cannot be changed after it is \emph{cooked}.
A \This-owned object is cooked
    when its owner is cooked (e.g., \code{foo.ownedD}).
Any other object is cooked
    when its constructor finishes (e.g., \code{d} and \code{foo}).
The intuition is that \code{ownedD} cannot leak and so the outside world
    cannot observe this longer cooking phase,
    whereas \code{d} is visible to the world after its constructor finishes and must not be mutated further.
The constructor on lines~\ref{OIGJEx:cj:raw}--\ref{OIGJEx:cj:raw:end} shows
    this difference between the assignments to \code{sameD} (line~\ref{OIGJEx:raw:sameD})
    and to \code{ownedD} (line~\ref{OIGJEx:raw:ownedD}):
    \code{sameD} can come from the outside world,
    whereas \code{ownedD} must be created inside \this.
Thus, \code{sameD} cannot be further mutated (line~\ref{OIGJEx:sameD:setTime})
    whereas \code{ownedD} can be mutated (line~\ref{OIGJEx:ownedD:setTime}) until its owner is cooked.

An object in a raw method, whose immutability parameter is \hI,
    is still considered raw (thus the modified body can still assign to its fields or call other raw methods)
    iff the object is \this or \this-owned.
Informally, we say that \Raw is \emph{transitive} only for \this or \this-owned objects.
For example, the receiver of the method call \code{sameD.setTime(\ldots)} is not \this nor \this-owned,
    and therefore the call on line~\ref{OIGJEx:sameD:setTime} is illegal;
    however, the receiver of \code{ownedD.setTime(\ldots)} is \this-owned,
    and therefore the call on line~\ref{OIGJEx:ownedD:setTime} is legal.


\subsection{Other Immutability Proposals}
\label{ss:others}

\paragraph{JAC} Similarly to the proposals in this chapter, JAC~\cite{KnieselT2001} has a
\JACreadonly{} keyword indicating transitive immutability, an implicit type
\JACreadonly{}~\mytt{T} for every class and interface \mytt{T} defined in the program, and a
\mutable{} keyword.
However, the other aspects of the two languages' syntax and semantics are
quite different.  For example, JAC provides a number of additional
features, such as a larger access right hierarchy (\mytt{readnothing} $<$
\mytt{readimmutable} $<$ \mytt{readonly} $<$ \mytt{writeable}) and additional keywords (such as
\mytt{nontransferrable}) that address other concerns than immutability.
The JAC authors propose implementing JAC by source rewriting, creating a  new
type \JACreadonly{}~\mytt{T} that has as
methods all methods of \mytt{T} that are declared with the keyword
\JACreadonly{} following the parameter list (and then compiling the result
with an ordinary Java compiler).  However, the return type of
any such method is \JACreadonly{}.
For example, if class \mytt{Person} has a
method \mytt{public Address getAddress() readonly}, then
\mytt{readonly} \mytt{Person} has method \mytt{public} \mytt{readonly}
  \mytt{Address getAddress() readonly}.  In other words, the return type of a
method call depends on the type of the receiver expression and may be a
supertype of the declared type, which violates Java's typing rules.
Additionally, JAC is either unsound for, or does not address, arrays of
\JACreadonly{} objects, casts, exceptions, inner classes, and subtyping.
JAC \JACreadonly{} methods may not change any static field of any class.
The JAC paper suggests that \JACreadonly{} types can be supplied as
type variables for generic classes without change to the GJ proposal, but
provides no details.  By
contrast to JAC, in Javari the return type of a method does not depend on
whether it is called through a read-only reference or a non-read-only one.
Both IGJ and OIGJ provide a thorough treatment of the generic types and immutability bringing the JAC generics proposal to its logical conclusion.

The above comments also explain why use of read-only interfaces in Java is
not satisfactory for enforcing read-only references.  A programmer could
define, for every class \jv{C}, an interface \jv{RO\_C} that declares the
read-only methods and that achieves transitivity through
changing methods that
returned (say) \jv{B} to return \jv{RO\_B}\@.  Use of \jv{RO\_C} could then
replace uses of Javari's \jv{readonly C}\@.  This is similar to JAC's
approach and shares similar problems.  For instance, to permit casting,
\jv{C} would need to implement \jv{RO\_C}, but some method return and
argument types are incompatible.  Furthermore, this approach does not allow
read-only versions of arrays or even \jv{Object}, since \jv{RO\_Object}
would need to be implemented by \jv{Object}.  It also forces information
about a class to be maintained in two separate files, and it does not
address run-time checking of potentially unsafe operations
or how to handle various other Java constructs.
Javari sidesteps these fundamental problems by extending
the Java type system rather than attempting to work within it.

\paragraph{Modes for Read-Only} Skoglund and Wrigstad~\cite{SkoglundW2001} take a different attitude
toward immutability than other work: ``In our point of [view], a
read-only method should only protect its enclosing object's transitive
state when invoked on a read reference but not necessarily when
invoked on a write reference.''  A \jv{read} (read-only) method may
behave as a \jv{write} (non-read-only) method when invoked via a
\jv{write} reference; a \jv{caseModeOf} construct permits run-time
checking of reference writeability, and arbitrary code may appear on
the two branches.  This suggests that while it can be proved that read
references are never modified, it is not possible to prove whether a
method may modify its argument.  In addition to read and write
references, the system provides \mytt{context} and \mytt{any}
references that behave differently depending on whether a method is
invoked on a read or write context.  Compared to this work and JAC,
Javari's, IGJ's and OIGJ's type parameterization gives a less ad
hoc and more disciplined way to specify families of declarations.

\paragraph{Immutability Specification} Pechtchanski and Sarkar~\cite{PechtchanskiS2002} provide a framework for
immutability specification along three dimensions: lifetime, reachability,
and context.  The lifetime is always the full scope of a reference, which
is either the complete dynamic lifetime of an object or, for parameter
annotations, the duration of a method call.  The reachability
is either shallow or deep.  The context is whether immutability applies in
just one method or in all methods.  The authors provide 5 instantiations of
the framework, and they show that immutability constraints enable
optimizations that can speed up some benchmarks by 5--10\%.

Even if all methods of a class are state preserving, the resulting
instances might not be immutable, because a mutable \this object could
escape the constructor and its fields can be mutated directly, for
instance, if the constructor stores all created objects in a static
set. The proposals in this chapter permit both of the lifetimes and
supplies deep reachability, which complements the shallow reachability
provided by Java's \kw{final} keyword.

\paragraph{Capabilities} Capabilities for sharing~\cite{BoylandNR2001} are intended to generalize
various other proposals for immutability and uniqueness.  When a new object
is allocated, the initial pointer has 7 access rights: read, write,
identity (permitting address comparisons), exclusive read, exclusive write,
exclusive identity, and ownership (giving the capability to assert rights).
Each (pointer)
variable has some subset of the rights.
These capabilities give an approximation and simplification of many other
annotation-based approaches.

\paragraph{Why not add read-only?} Boyland~\cite{Boyland2005} explains ``Why we should not add
\code{readonly} to Java (yet)'' and concludes that readonly does not
address observational exposure, i.e., modifications on one side of an
abstraction boundary that are observable on the other side.  IGJ's
immutable objects address such exposure because their state cannot
change, e.g., an immutable address in a person object can be safely shared
among many person objects.  Sometimes it is impossible to avoid
observational exposure, e.g., when a container changes and iterators
to the inside of the container exists.  Java designed its iterator
classes to be \emph{fail-fast}, i.e., the iterator will fail if the
collection is mutated (which cannot happen in immutable collections).

Boyland's second criticism was that the \textit{transitivity}
principle (see end of Section~\ref{s:immutability-current})
should be selectively applied by the
designer, because, ``the elements in the container are not notionally
part of the container''~\cite{Boyland2005}.  In \Joe, IGJ, and OIGJ, a programmer can
solve this problem by using a different immutability for the container
and its elements.

\paragraph{Effects} Effect systems~\cite{LucassenG88,TalpinJ92,NiNi99tes} specify what state
(in terms of regions or of individual variables) can be read and modified
by a procedure; they can be viewed as labeling (procedure) types with
additional information, which the type rules then manipulate.  Type systems
for immutability can be viewed as a form of effect system.  The proposals in this chapter are
finer-grained than typical effect systems, operate over references rather
than values, and consider all state reachable from a reference.

\paragraph{Universes} Universe Types~\cite{MuellerPoetzsch-Heffter01a} were the first ownership type system to provide support for read-only references by introducing ``owners as modifiers'' discipline. Here, if an object does not have a right to access an object because of ownership restrictions, it is still allowed a read-only reference to such object. This greatly improved the expressiveness of the language albeit weakened the ownership guarantees - as a result both OIGJ and \Joe tried to mitigate these issues by providing a more granular interaction between immutability and ownership properties in a language.
Finally, the functional methods of Universes~\cite{MuellerPoetzsch-Heffter01a} are
pure methods that are not allowed to modify anything (as opposed to merely
not being allowed to modify the receiver object).

\paragraph{Immutable Objects}

Immutable Objects for a Java-like Language (\textbf{IOJ})~\cite{HaackPSS2007}
    associates with each type its mutability and owner.
In contrast to OIGJ, IOJ does not have generics,
    nor readonly \emph{references}. %
Moreover, in IOJ, the constructor cannot leak a reference to \this.
%
Haack and Poll~\cite{HaackPSS2007} later added flexible initialization of immutable objects~\cite{haack:2009:obj-imm},
    i.e., an immutable object may still be mutated after its constructor returns.
They use the annotations \code{RdWr}, \code{Rd}, \code{Any}, and \code{myaccess},
    which corresponds to our \code{Mutable}, \code{Immut}, \code{ReadOnly}, and \code{I}.
In addition, they have an inference algorithm that automatically infers the end of object initialization phases.
(Their algorithm infers which variables are \code{Fresh(n)}, which resembles our \code{Raw}.
    However, the programmer cannot write the \code{Fresh} annotation explicitly.)

\paragraph{Immutability Inference} Porat et al.~\cite{PoratBKM2000} provide a type inference that
determines (deep) immutability of fields and classes.  (Foster et
al.~\cite{FosterFFA99} provide a type inference for C's
(non-transitive) \Cconst{}.)  A field is defined to be immutable if
its value never changes after initialization and the object it refers
to, if any, is immutable.  An object is defined to be immutable if all
of its fields are immutable.  A class is immutable if all its
instances are.  The analysis is context-insensitive in that if a type
is mutable, then all the objects that contain elements of that type
are mutable.  Libraries are neither annotated nor analyzed: every
virtual method invocation (even \mytt{equals}) is assumed to be able
to modify any field.  The paper discusses only class (static)
variables, not member variables.  The technique does not apply to
method parameters or local variables, and it focuses on object rather
than reference immutability, as in Javari.  An experiment indicted
that 60\% of static fields in the Java 2 JDK runtime library are
immutable.

\paragraph{Constructing Immutable Objects} Non-null types~\cite{FahndrichL2003,fahndrich:2007:delayed,qi:2009:popl,summers:2011:oopsla} has a similar challenge that IGJ
has in constructing immutable objects: a partially-initialized object
may escape its constructor.  IGJ uses \AssignsFieldsAnnot to mark a
constructor of immutable objects, and a partially initialized object
can escape only as \ReadOnly.  Non-null types uses a \code{Raw}
annotation \emph{on references} that might point to a
partially-initialized object, and \emph{on methods} to denote that the
receiver can be \code{Raw}.  A non-null field of a \code{Raw} object
has different lvalue and rvalue: it is possible to assign only
non-null values to such field, whereas reading from such field may
return \code{null}.  Similarly to IGJ, non-null types
cannot handle cyclic data-structures, %with non-null fields
express the staged initialization paradigm in which the construction
of an object continues after its constructor finishes. OIGJ~\cite{zibin:2010:oigj} however addressed most of these IGJ shortcomings.

\paragraph{Frozen Objects} Leino et al.~\cite{LeinoMW2008} show how ownership can help support immutability
by allowing programmers to decide when the object should become immutable. This system
takes a verification approach rather than a simple type checker. Frozen Objects show
how flexible the initialization stage can potentially be in the presence of ownership and immutability,
while, for example, OIGJ shows how much flexibility can be achieved while staying at the type checking level.

\paragraph{Other Proposals} Huang et al.~\cite{HuangZS2007:cJ} propose an extension of Java
(called cJ) that allows methods to be provided only under some static
subtyping condition.  For instance, a cJ generic class,
\code{Date<I>}, can define
%
\begin{java}
<I extends Mutable>? void setDate(^($\cdots$)^)
\end{java}
%
which will be provided only when the type provided for parameter~\IP
is a subtype of \Mutable.  Designing IGJ on top of cJ would make
\methodrule redundant, at the cost of replacing IGJ's method
annotations with cJ's conditional method syntax.  The rest of IGJ's
typing rules will remain the same.

Finally, IGJ uses the type system to check immutability statically.
Controlling immutability at runtime (for example using assertions or
Eiffel-like contractual obligations) falls outside the scope of this
chapter.


\subsection{Summary of Immutability Work}


\newcommand{\colwidth}{p{1em}}
\newcommand{\tilt}[1]{\rotatebox{80}{#1}}
\newcommand{\YS}[1][]{\ensuremath{\surd^{#1}}}
\newcommand{\NO}[1][]{\ensuremath{\times^{#1}}}
\newcommand{\SEP}[1]{%
  \vspace{-1ex}\\%
  \multicolumn{11}{@{}p{.72\linewidth}@{}}{\hrulefill~~\textit{#1}~~\hrulefill} \\[.5ex]%
}

%% MDE: I changed this from a table to a figure because when it's the
%% only table, readers have to look at every page to find it.  When it's
%% one of many figures, readers can find it relative to other figures.
\begin{figure}[t]
\footnotesize
  \begin{tabular}{@{}l\colwidth\colwidth\colwidth\colwidth\colwidth\colwidth\colwidth\colwidth\colwidth\colwidth@{}}
    \bf Feature &\tilt{OIGJ}
                 &\tilt{\Joe}
                   & \tilt{SafeJava} % \cite{boyapati-thesis}}
                      & \tilt{Universes} % \cite{MPH99a,DM05,DDM07}}
                             & \tilt{Jimuva} % \cite{HPSS07}}
                                   &  \tilt{Javari} % \cite{TE05}}
                                            & \tilt{IGJ} % \cite{ZPAKE07}}
                                                  & \tilt{ModeJava} % \cite{SW01,SW02}}
                                                        & \tilt{JAC}  % \cite{KT01,jac99}} 
                                                              & \tilt{EO}  \\[-1ex]% \cite{PL06}
    % --------------------------------------------------------------------------------
    \SEP{Expressiveness} 
    % --------------------------------------------------------------------------------
    Staged const.    & \NO[8] & \YS & \YS    &  \NO    & \NO    &   \NO  &  \NO   &  \NO   & \NO   & \NO \\
    Fract. perm.     & \NO    & \YS & \NO    &  \NO    & \NO    &   \NO  &  \NO   &  \NO   & \NO   & \NO \\
    Non-rep fields   & \YS    & \YS & \YS[1] &  \YS[1] & \YS[1] & \NO[2] & \NO[2] &  \NO   & \NO   & \NO \\
%    ~\\
    % --------------------------------------------------------------------------------
    \SEP{Flexible Alias Protection Modes} 
    % --------------------------------------------------------------------------------
    \it arg          & \YS & \YS & \NO[3] &  \NO & \NO[3] &   \NO[3]  & \NO[3]  & \NO[3] & \NO  & \NO \\
    \it rep          & \YS & \YS & \YS &  \YS & \YS &   \NO  &  \NO&  \NO& \NO  & \YS \\
    \it free         & \NO & \YS & \YS &  \YS & \NO &   \NO  &  \NO&  \NO& \NO  & \NO \\
    \it val $^4$     & \NO & \NO & \NO &  \NO & \NO &   \NO  &  \NO&  \NO& \NO  & \NO \\
    \it var          & \YS & \YS & \YS &  \YS & \YS &   \YS  &  \YS&  \YS& \YS  & \YS \\
    % --------------------------------------------------------------------------------
    \SEP{Immutability} 
    % --------------------------------------------------------------------------------
    Class            & \YS & \YS & \NO &  \NO & \YS &   \YS  &  \YS&  \NO[5]& \NO[5]   & \NO \\
    Object           & \YS & \YS & \YS &  \NO & \YS &   \NO  &  \YS&  \NO& \NO         & \NO \\
    Context-based    & \YS & \YS & \NO &  \YS & \NO &   \NO[6]&  \NO[6]&  \NO[6]& \NO  & \NO \\
    Read-only ref.   & \YS & \YS & \NO &  \YS & \NO &   \YS  &  \YS&  \YS& \YS         & \YS \\
% ALEX: THE BELOW NEEDS SANITY CHECKING BY SOMEONE ELSE AND MAYBE DESCRIPTION IN TEXT?
    Shallow Immutability  & \YS & \YS & \NO & \YS & \NO & \YS  & \YS & \YS & \YS  & \YS \\
    Deep Immutability  & \YS & \YS & \NO & \NO & \NO & \YS  & \YS & \NO & \NO  & \NO \\
    Abstract Value Immutability  & \YS & \YS & \NO & \YS & \NO & \YS  & \YS & \YS & \YS  & \YS \\
    Concrete Representation Immutability  & \YS & \YS & \NO & \YS & \NO & \NO  & \NO & \NO & \NO  & \NO \\
    % --------------------------------------------------------------------------------
    \SEP{Confinement and Alias Control} 
    % --------------------------------------------------------------------------------
    OT               & \YS & \YS &  \YS    &  \YS & \YS &   \NO  &  \NO&  \NO& \NO & \YS \\
    OP meths         & \YS & \YS &  \YS    &  \YS & \YS &   \NO  &  \NO&  \NO& \NO & \NO \\
    OAM              & \NO & \NO &  \NO &  \YS & \NO &   \NO  &  \NO&  \NO& \NO & \YS \\
    OAD              & \NO[7] & \YS &  \NO[7]  &  \NO & \NO &   \NO  &  \NO&  \NO& \NO & \NO \\
    Uniqueness       & \NO & \YS &  \YS    &  \YS & \NO &   \NO  &  \NO&  \NO& \NO & \NO \\
    ~\\
    % --------------------------------------------------------------------------------
  \end{tabular}
  \caption{Brief overview of related work. OT=ownership types,
    OP=owner polymorphic, OAM=owner-as-modifier,
    OAD=owner-as-dominator, EO=Effective Ownership.
  $^1$) not as powerful as there is no owner nesting; two non
        sibling lists cannot share \emph{mutable} data elements;
  $^2$) mutable fields can be used to store a reference to \code{this} and
        break read-only;
  $^3$) no modes on owners, and hence no immutable parts of objects;
  $^4$) none of the systems deal with value semantics for complex objects;
  $^5$) if all methods of a class are read-only the class is
        effectively immutable;
  $^6$) limited notion of contexts via \this-mutability;
  $^7$) allows breaking of owners-as-dominators with inner
        classes.
  $^8$) \kw{Raw} constructors can construct both mutable and immutable
        objects, but once the constructor returns immutability
        is fixed.
  }
%  \mde{Add, to the table, whether each supports shallow immutability, deep
%    immutability, or both; also add whether each supports abstract
%    value immutability, concrete representation immutability, or both.}
  \label{fig:features}
\end{figure}


Figure~\ref{fig:features} summarizes several proposals and their
supported features. The systems included in the table represent
the state of the art of read-only and immutable. Except \Joe, the
table includes (in order) SafeJava \cite{boyapati-thesis},
Universes \cite{MPH99a,DM05,DDM07,MR07}, Jimuva \cite{HPSS07},
Javari \cite{TE05}, IGJ \cite{ZPAKE07}, JAC \cite{KT01}, ModeJava
\cite{SW02} and Effective Ownership \cite{LP06}. We now discuss
the different features in the table.

\Joe and SafeJava support staged construction of immutables.

Boyland suggests that copying
rights may lead to observational exposure and proposes that the
rights instead be split. Only the one with a complete set of
rights may \mify an object. SafeJava does not support borrowing to
immutables and hence cannot model fractional permissions. It is
unclear how allowing borrowing to immutables in SafeJava would
affect the system, especially in the presence of back doors that
break encapsulation. 

To be able to retrieve writable objects from a read-only
list, the elements in the list cannot be part of the list's
representation. \Joe, Universes, Jimuva and SafeJava can express
this through ownership types. Only OIGJ and \Joe systems, thanks to owner
nesting information, allow two non-sibling lists to share mutable
data elements. Javari and IGJ allow this through ad-hoc mutable
fields which can circumvent read-only if an object stores a
reference to itself in a mutable field.

The alias modes proposed by Noble et~al.~\cite{NVP98}. Here we only
describe how the modes have been interpreted for the purpose of
Figure~\ref{fig:features}. The \emph{rep} mode denotes a reference belonging to an object's
representation and so should not appear in its interface. A defensive
interpretation of \emph{arg} is that all systems that have object or
class immutability partially support \emph{arg}, but only OIGJ and \Joe systems
support \emph{parts} of an object being immutable. The \emph{free}
mode, interpreted as being equal to uniqueness, is supported by \Joe
and SafeJava. No system handles \emph{val}ue semantics except for
primitive types. The \emph{var} aliasing mode expresses non-\emph{rep}
references which may be aliased and changed freely as long as they do
not interfere with the other modes, for example, in assignments.

%%% Local Variables: 
%%% TeX-command-default: "PDF"
%%% End: 

% LocalWords:  Tschantz assignability readonly templating templated RO ppt mutD
% LocalWords:  PptTopLevel classfile immutD ReadOnly roD Bracha Igarashi GJ STL
% LocalWords:  const getFieldFoo IGJ's rvalue wildcards Drossopoulou's addFirst
% LocalWords:  Wrigstad's ListWriter strictlyoutside mutateList ListReader quo
% LocalWords:  mutateElements createList Boyland's cJ Immut imD sameD ownedD im
% LocalWords:  publicD cJ's readonlyMethod mutatingMethod contravariant OAD JAC
% LocalWords:  setTime readnothing readimmutable writeable nontransferrable EO
% LocalWords:  getAddress JAC's Skoglund Wrigstad caseModeOf OIGJ's Sarkar arg
% LocalWords:  Pechtchanski Boyland Porat setDate SafeJava Jimuva ModeJava OAM
% LocalWords:  Fract
